package launcher;

import java.io.File;
import java.io.PrintStream;
import java.util.ArrayList;
import java.util.Scanner;
import java.util.StringTokenizer;

import CTL.CTLArriere;
//import CTL.CTLAvant;

import rdp.RdP;
import systeme.AlgoGrapheRdP;
import systeme.GrapheRdP;

public class LauncherApplication {

	static String[] operateur = { "!", "||", "&&", "AX", "EX", "AU", "EU" };

	public static String affiche(boolean[] b) {
		StringBuffer res = new StringBuffer();
		int count = 0;
		if (b.length != 0) {
			res.append(" \nListe des états vérifiant la formule { ");
			for (int i = 0; i < b.length; i++) {
				if (b[i]) {
					res.append((i + 1) + " ");
					count++;
				}
			}
			res.append("}");
		}

		StringBuffer res2 = new StringBuffer();
		res2.append("Nombres d'états : " + count);
		res2.append(res.toString());
		return res2.toString();

	}

	public static String afficheEtat(boolean[] b, int etat) {

		StringBuffer res = new StringBuffer();
		res.append("Valeur de la formule pour l'état " + (etat + 1) + " : "
				+ b[etat]);
		return res.toString();
	}

	public static boolean isOperateur(String op) {

		int taille = operateur.length;
		boolean trouve = false;
		int i = 0;

		while (!trouve && i < taille) {

			trouve = op.equalsIgnoreCase(operateur[i]);
			i++;
		}

		return trouve;
	}

	public static boolean[] evaluer(String formule, CTLArriere ctl) {

		StringTokenizer tokenizer = new StringTokenizer(formule, " ");
		String tok;

		ArrayList<String> operateur = new ArrayList<String>();
		ArrayList<boolean[]> operande = new ArrayList<boolean[]>();

		while (tokenizer.hasMoreTokens()) {

			tok = tokenizer.nextToken();

			if (isOperateur(tok)) {

				// On ajoute l'opérateur
				operateur.add(tok);

			} else {

				tok = tokenizer.nextToken();
				operande.add(ctl.prop(Integer.parseInt(tok)));
			}

			// System.out.println( tok + " Op ? " + isOperateur(tok));
		}

		int i = 0;

		String op;
		boolean[] operandeTemp;

		while (i < operateur.size()) {

			op = operateur.get(i);

			operandeTemp = operande.remove(operande.size() - 1);

			if (op.equalsIgnoreCase("!")) {
				// Si c'est la négation

				operande.add(ctl.neg(operandeTemp));

			} else {

				if (op.equalsIgnoreCase("AX")) {

					operande.add(ctl.AX(operandeTemp));

				} else {

					if (op.equalsIgnoreCase("EX")) {

						operande.add(ctl.EX(operandeTemp));

					} else {

						if (op.equalsIgnoreCase("||")) {

							operande.add(ctl.or(operandeTemp,
									operande.remove(operande.size() - 1)));

						} else {

							if (op.equalsIgnoreCase("&&")) {

								operande.add(ctl.and(operandeTemp,
										operande.remove(operande.size() - 1)));

							} else {

								if (op.equalsIgnoreCase("AU")) {

									operande.add(ctl.AU(operandeTemp, operande
											.remove(operande.size() - 1)));

								} else {

									if (op.equalsIgnoreCase("EU")) {

										operande.add(ctl.EU(
												operandeTemp,
												operande.remove(operande.size() - 1)));

									}
								}

							}

						}
					}
				}

			}

			i++;
		}

		return operande.get(0);

	}

	static final String AIDE = "propriete \t ::= propriete || propriete"
			+ "\t| propriete && propriete" + "\t| ! propriete |\n"
			+ "          \t   | propriete -> propriete"
			+ "\t| propriete <-> propriete" + "\t| (propriete)\n"
			+ "          \t   | $place" + "\t\t\t| enable($transition)\n"
			+ "          \t   | dead" + "\t\t\t| initial\n"
			+ "          \t   | EX propriete" + "\t\t| AX propriete\n"
			+ "          \t   | EF propriete" + "\t\t| AF propriete\n"
			+ "          \t   | EG propriete" + "\t\t| AG propriete\n"
			+ "          \t   | E(proprite U propriete)"
			+ "\t| A(propriete U propriete)\n";

	public static void ecrire(String fichier, String texte) {
		try {
			PrintStream f = new PrintStream(new File(fichier));
			f.print(texte);
			f.close();
		} catch (Exception e) {
			System.err.println("Probleme d'ecriture !");
		}
	}

	public static void main(String[] args) {
		Scanner sc = new Scanner(System.in);
		String ligne = "";
		StringTokenizer tokenizer;
		String mot;
		int nbMot;
		GrapheRdP graphe = null;
		AlgoGrapheRdP algo;
		RdP rdp = null;

		while (!ligne.equalsIgnoreCase("exit")) {

			System.out.println("Entrez une commande");
			ligne = sc.nextLine();

			tokenizer = new StringTokenizer(ligne, " ");

			while (tokenizer.hasMoreTokens()) {

				mot = tokenizer.nextToken();

				if (mot.equalsIgnoreCase("load")) {

					nbMot = tokenizer.countTokens();

					if (nbMot < 1) {

						System.out.println("Erreur fichier manquant");

					} else {

						if (nbMot > 1) {

							System.out.println("Trop d'arguments");

						} else {

							mot = tokenizer.nextToken();

							try {

								rdp = new RdP(mot);

								System.out.println("Nombre de places : "
										+ rdp.place.length
										+ "\nNombre de transitions : "
										+ rdp.transition.length);
							} catch (Exception e) {
								// TODO Auto-generated catch block
								System.out.println(e.toString());
							}
						}
					}

				} else {

					if (mot.equalsIgnoreCase("graphe")) {

						if (rdp == null) {
							System.out
									.println("Le fichier n'a pas était chargé");

						} else {

							try {
								algo = new AlgoGrapheRdP(rdp);

								graphe = algo.grapheRdP();

								System.out.println("Nombre d'états : "
										+ graphe.nbEtat + " Nombre d'arcs : "
										+ graphe.nbTransition);
							} catch (Exception e) {
								// TODO Auto-generated catch block
								System.out.println(e.toString());
							}

						}

					} else {

						if (mot.equalsIgnoreCase("look")) {

							nbMot = tokenizer.countTokens();

							if (nbMot > 1) {

								System.out
										.println("Trop d'arguments en paramètre");

							} else {

								if (nbMot < 1) {

									System.out.println("Pas assez d'arguments");

								} else {

									if (graphe == null) {

										System.out
												.println("Le calcul du graphe n'a pas était effectué");

									} else {

										try {
											int etat = Integer
													.parseInt(tokenizer
															.nextToken());
											etat--;

											if (etat < 0
													|| etat >= graphe.nbEtat) {

												System.out
														.println("Entier correspondant à aucun état");

											} else {

												boolean marquage[] = graphe
														.recupererEtat(etat);
												System.out
														.println(rdp
																.toStringMarquage(marquage));
											}

										} catch (NumberFormatException e) {

											System.out
													.println("Vous n'avez pas rentrer un entier");
										}
									}
								}
							}

						} else {

							if (mot.equalsIgnoreCase("succ")) {

								nbMot = tokenizer.countTokens();

								if (nbMot > 1) {

									System.out
											.println("Trop d'arguments en paramètre");

								} else {

									if (nbMot < 1) {

										System.out
												.println("Pas assez d'arguments");

									} else {

										if (graphe == null) {

											System.out
													.println("Le calcul du graphe n'a pas était effectué");

										} else {

											try {
												int etat = Integer
														.parseInt(tokenizer
																.nextToken());
												etat--;

												if (etat < 0
														|| etat >= graphe.nbEtat) {

													System.out
															.println("Entier correspondant à aucun état");

												} else {

													ArrayList<Integer> succ = graphe
															.recupererSucc(etat);

													if (succ.size() == 0) {

														System.out
																.println("Pas de successeurs");
													} else {

														for (int t = 0; t < succ
																.size(); t++)
															System.out
																	.println("N"
																			+ (etat + 1)
																			+ " -> N"
																			+ (succ.get(t) + 1)
																			+ "\n");

													}
												}

											} catch (NumberFormatException e) {

												System.out
														.println("Vous n'avez pas rentrer un entier");
											}
										}
									}
								}

							} else {

								if (mot.equalsIgnoreCase("todot")) {

									nbMot = tokenizer.countTokens();

									if (nbMot > 1) {

										System.out
												.println("Trop d'arguments en paramètre");

									} else {

										if (nbMot < 1) {

											System.out
													.println("Pas assez d'arguments en paramètre");

										} else {

											if (graphe != null) {

												mot = tokenizer.nextToken();
												System.out.println(mot);
												ecrire(mot, graphe.toDot());

											} else {

												System.out
														.println("Le graphe n'a pas encore était calculé");
											}
										}
									}

								} else {

									if (mot.equalsIgnoreCase("ctl")) {

										nbMot = tokenizer.countTokens();

										if (nbMot < 1) {

											System.out
													.println("Pas assez d'arguments");

										} else {

											if (nbMot > 2) {

												System.out
														.println("Trop d'arguments");

											} else {

												mot = tokenizer.nextToken();
												CTLArriere ctl = new CTLArriere(graphe);

												try {

													String formule = rdp
															.ctl(mot);

													if (formule == null) {

														System.out
																.println(AIDE);

													} else {

														// System.out
														// .println(formule);
														boolean[] etats = evaluer(
																formule, ctl);

														nbMot = tokenizer
																.countTokens();

														if (nbMot == 1) {

															int etat = Integer
																	.parseInt(tokenizer
																			.nextToken());
															etat--;

															if (etat >= etats.length
																	|| etat < 0) {

																System.out
																		.println("Erreur l'état n'est pas compris entre 1 et "
																				+ etats.length);
															} else {

																System.out
																		.println(afficheEtat(
																				etats,
																				etat));

															}

														} else {

															ecrire("test.dot",
																	graphe.toDot(etats));
															System.out
																	.println(affiche(etats));
														}

													}

												} catch (Exception e) {

													System.out
															.println("Formule ctl incorrecte");

												}
											}
										}

									} else {

										if (mot.equalsIgnoreCase("ctltodot")) {

											nbMot = tokenizer.countTokens();

											if (nbMot > 2) {

												System.out
														.println("Trop d'arguments en paramètre");

											} else {

												if (nbMot < 2) {

													System.out
															.println("Pas assez d'arguments en paramètre");

												} else {

													if (graphe != null) {
														
														mot = tokenizer
																.nextToken();

														String nomFichier = tokenizer
																.nextToken();
														
														CTLArriere ctl = new CTLArriere(
																graphe);

														try {

															String formule = rdp
																	.ctl(mot);

															if (formule == null) {

																System.out
																		.println(AIDE);

															} else {

																// System.out
																// .println(formule);
																boolean[] etats = evaluer(
																		formule,
																		ctl);
																ecrire(nomFichier,
																		graphe.toDot(etats));
																
																System.out
																		.println("Write Success");
															}

														} catch (Exception e) {

															System.out
																	.println("Formule ctl incorrecte");

														}

													} else {

														System.out
																.println("Le graphe n'a pas encore était calculé");
													}
												}
											}

										}else{
											if (mot.equalsIgnoreCase("pred")) {

												nbMot = tokenizer.countTokens();

												if (nbMot > 1) {

													System.out
															.println("Trop d'arguments en paramètre");

												} else {

													if (nbMot < 1) {

														System.out
																.println("Pas assez d'arguments");

													} else {

														if (graphe == null) {

															System.out
																	.println("Le calcul du graphe n'a pas était effectué");

														} else {

															try {
																int etat = Integer
																		.parseInt(tokenizer
																				.nextToken());
																etat--;

																if (etat < 0
																		|| etat >= graphe.nbEtat) {

																	System.out
																			.println("Entier correspondant à aucun état");

																} else {

																	ArrayList<Integer> pred = graphe
																			.recupererPred(etat);

																	if (pred.size() == 0) {

																		System.out
																				.println("Pas de predecesseurs");
																	} else {

																		for (int t = 0; t < pred
																				.size(); t++)
																			System.out
																					.println("P"
																							+ (etat + 1)
																							+ " -> P"
																							+ (pred.get(t) + 1)
																							+ "\n");

																	}
																}

															} catch (NumberFormatException e) {

																System.out
																		.println("Vous n'avez pas rentrer un entier");
															}
														}
													}
												}

											}
										}
									}
								}
							}
						}
					}
				}
			}

		}
	}

}
